Step of Proof: before-adjacent 11,40

Inference at * 2 1 1 2 1 3 1 
Iof proof for Lemma before-adjacent:



1. T : Type
2. T List
3. u : T
4. v : T List
5. xy:T.
5. no_repeats(T;v adjacent(T;v;x;y (z:Tz before y  v  (z before x  v  (z = x)))
6. x : T
7. y : T
8. no_repeats(T;v)
9. (u  v)
10. 0 < ||v||
11. x = u
12. y = hd(v)
13. z : T
14. z before y  v
15. hd(v) before z  v
16. z before hd(v v
  ((z = u & (x  v))  z before x  v (z = x
latex

 by ((RevHypSubst (-5) (-1)) 
CollapseTHEN (Auto)) 
latex


C.


Definitionshd(l), , a < b, no_repeats(T;l), type List, Type, x before y  l, x:AB(x), x:AB(x), s = t, t  T, A, P  Q, False
Lemmasnot wf, l before wf

origin